i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da), T:Type.
(k:Knd. (k  ecl-trans-ks(ecl-trans(A)))  (fpf-dom(Kind-deq; k; da)))
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 (T = ecl-trans-type(ecl-trans(A)))
 R-compat{i:l}
 R-compat(ecl-machine1{ecl:ut2}
 R-compat(ecl-machine1(i; ds; da; A);
 R-compat(ecl-machine3(ds;
 R-compat(ecl-machine3(da;
 R-compat(ecl-machine3(mkid{ecl:ut2};
 R-compat(ecl-machine3(T;
 R-compat(ecl-machine3(ecl-trans-ks(ecl-trans(A));
 R-compat(ecl-machine3(ecl-trans-a(ecl-trans(A));
 R-compat(ecl-machine3(snd)) 

latex

Definitions

True, T, False, A  B, top, P  Q, suptype(S; T), subtype(S; T), A c B, x:A. B(x), prop{i:l}, x. t(x), IdLnk, x(s), t.1, ma-valtype(da; k), decl-state(ds), t  T, R-state-var-init(i; ds; da; x; T; v; ks; tr), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-a(v), ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-trans-type(A), mkid{$x:ut2}, A, ecl-trans-ks(v), (x  l), P  Q, Knd, Id, x:A. B(x), P  Q, P  Q, , ecl-trans-tuple{i:l}(ds; da)

Lemmas

ecl wf, msg-spec wf, ecl-trans-ks wf, Knd wf, not wf, ecl-trans-type wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, Rinit-lnk-tags-compat, fpf-compatible-singles, fpf-compatible-single2, fpf-compatible-self, fpf-compatible-join2, fpf-compatible-join, top wf, fpf-cap-void-subtype, deq wf, Id wf, fpf wf, true wf, squash wf, rcv wf, Kind-deq wf, fpf-cap wf, select wf, length wf1, R-state-var-lnk-tags-compat2, R-compat-Rplus-sq, rationals wf, Rinit wf, fpf-compatible-single, R-state-var wf, Rplus wf, bool wf, ma-valtype wf, decl-state wf, nat wf, ecl-m3 wf, ecl-tags wf, id-deq wf, fpf-single wf3, fpf-join wf, R-lnk-tags wf, l member wf, msg-spec-links wf, idlnk-deq wf, IdLnk wf, remove-repeats wf, R-compat-Rall, ecl-trans-tuple wf, ecl-trans wf